$\forall$$A$:Type, $P$:($A$$\rightarrow$Prop), $f$:$a$:\{$a$:$A$$\mid$ $P$($a$) \} fp$\rightarrow$ Type. $f$ $\in$ $a$:$A$ fp$\rightarrow$ Type